Nuprl Lemma : free-from-atom-subtype
11,40
postcript
pdf
A
,
B
:Type. (
A
r
B
)
(
x
:
A
,
a
:Atom1.
x
:
A
||
a
x
:
B
||
a
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
free-from-atom
wf1
origin
A, B:Type. (A 
r B) 
(x:A, a:Atom1. x:A||a x:B||a) A, B:Type. (A r B) (x:A, a:Atom1. x:A||a x:B||a) 
T Qx:A. B(x)